Inference at * 2 0 
Iof proof for Lemma select nth tl:



1. T : Type
2. T List
3. u : T
4. v : T List
5. n:{0...||v||}, i:{0..(||v|| - n)}. nth_tl(n;v)[i] = v[(i+n)]
  n:{0...||v||+1}, i:{0..((||v||+1) - n)}. nth_tl(n;[u / v])[i] = [u / v][(i+n)] 

latex

 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{3:n,
 by PERMUTE{4:n,
 by PERMUTE{5:n,
 by PERMUTE{6:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{10:n,
 by PERMUTE{13:n,
 by PERMUTE{11:n,
 by PERMUTE{14:n,
 by PERMUTE{15:n,
 by PERMUTE{16:n,
 by PERMUTE{17:n,
 by PERMUTE{18:n,
 by PERMUTE{16:n,
 by PERMUTE{15:n,
 by PERMUTE{19:n,
 by PERMUTE{20:n,
 by PERMUTE{21:n} 

latex

 1: .....wf..... NILNIL

 1: 6. n : {0...||v||+1}
 1: 7. {0..((||v||+1) - n)}
 1:   n z 0  
 2: .....wf..... NILNIL

 2: 6. n : {0...||v||+1}
 2: 7. {0..((||v||+1) - n)}
 2:     Type
 3: .....wf..... NILNIL

 3: 6. n : {0...||v||+1}
 3: 7. {0..((||v||+1) - n)}
 3: 8. n z 0 = tt
 3:   (n z 0 = tt)  
 4: .....wf..... NILNIL

 4: 6. n : {0...||v||+1}
 4: 7. {0..((||v||+1) - n)}
 4: 8. n z 0 = tt
 4:   (n z 0)  
 5: .....wf..... NILNIL

 5: 6. n : {0...||v||+1}
 5: 7. {0..((||v||+1) - n)}
 5: 8. n z 0 = tt
 5:   (n  0)  
 6: .....wf..... NILNIL

 6: 6. n : {0...||v||+1}
 6: 7. {0..((||v||+1) - n)}
 6: 8. n z 0 = tt
 6:   n z 0  
 7: .....wf..... NILNIL

 7: 6. n : {0...||v||+1}
 7: 7. {0..((||v||+1) - n)}
 7: 8. n z 0 = tt
 7:   n  
 8: .....wf..... NILNIL

 8: 6. n : {0...||v||+1}
 8: 7. {0..((||v||+1) - n)}
 8: 8. n z 0 = tt
 8:   0  
 9: .....truecase..... NILNIL

 9: 6. n : {0...||v||+1}
 9: 7. i : {0..((||v||+1) - n)}
 9: 8. n  0
 9:   [u / v][i] = [u / v][(i+n)]
 10: .....wf..... NILNIL

 10: 6. n : {0...||v||+1}
 10: 7. {0..((||v||+1) - n)}
 10: 8. n z 0 = ff
 10:   (n z 0 = ff)  
 11: .....wf..... NILNIL

 11: 6. n : {0...||v||+1}
 11: 7. {0..((||v||+1) - n)}
 11: 8. n z 0 = ff
 11:   (0 <z n)  
 12: .....wf..... NILNIL

 12: 6. n : {0...||v||+1}
 12: 7. {0..((||v||+1) - n)}
 12: 8. n z 0 = ff
 12:   (0 < n)  
 13: .....wf..... NILNIL

 13: 6. n : {0...||v||+1}
 13: 7. {0..((||v||+1) - n)}
 13: 8. n z 0 = ff
 13:   ((n z 0))  
 14: .....wf..... NILNIL

 14: 6. n : {0...||v||+1}
 14: 7. {0..((||v||+1) - n)}
 14: 8. n z 0 = ff
 14:   n z 0  
 15: .....wf..... NILNIL

 15: 6. n : {0...||v||+1}
 15: 7. {0..((||v||+1) - n)}
 15: 8. n z 0 = ff
 15:   n  
 16: .....wf..... NILNIL

 16: 6. n : {0...||v||+1}
 16: 7. {0..((||v||+1) - n)}
 16: 8. n z 0 = ff
 16:   0  
 17: .....antecedent..... NILNIL

 17: 6. n : {0...||v||+1}
 17: 7. {0..((||v||+1) - n)}
 17: 8. n z 0 = ff
 17:   True
 18: .....wf..... NILNIL

 18: 6. n : {0...||v||+1}
 18: 7. {0..((||v||+1) - n)}
 18: 8. n z 0 = ff
 18: 9. ((n z 0)) = (0 <z n)
 18:    = 
 19: 

 19: 6. n : {0...||v||+1}
 19: 7. i : {0..((||v||+1) - n)}
 19: 8. 0 < n
 19:   nth_tl(n - 1;v)[i] = [u / v][(i+n)]
 20: .....wf..... NILNIL

 20: 6. n : {0...||v||+1}
 20:   {0..((||v||+1) - n)}  Type
 21: .....wf..... NILNIL

 21:   {0...||v||+1}  Type
 .

Definitions

[], rec-case(a) of [] => s | x::y => z.t(x;y;z), {x:A| B(x)} , b, i <z j, a < b, inr x , case b of inl(x) => s(x) | inr(y) => t(y), x:A  B(x), b, A  B, , Ax, , inl x , left + right, i z j, x.A(x), f(a), x:AB(x), [car / cdr], n+m, l[i], s = t, n - m, {i..j}, ||as||, #$n, {i...j}, type List, Type, , Unit, , True, T, ff, P  Q, P & Q, P  Q, tt, P  Q, t  T, tl(l), if b then t else f fi , Y, nth_tl(n;as), x:A. B(x)

Lemmas

assert of lt int, bnot of le int, bool wf, true wf, squash wf, assert wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity